Gatlab.jl

@theory

• the theory of categories can be defined by:

@theory ThCategory begin
  @op begin
    (→) := Hom
    (⋅) := compose
  end
  Ob::TYPE
  Hom(dom::Ob, codom::Ob)::TYPE
  id(A::Ob)::(A → A)
  compose(f::(A → B), g::(B → C))::(A → C) ⊣ [A::Ob, B::Ob, C::Ob]
  (f ⋅ g) ⋅ h == f ⋅ (g ⋅ h) ⊣ [A::Ob, B::Ob, C::Ob, D::Ob,
                                f::(A → B), g::(B → C), h::(C → D)]
  f ⋅ id(B) == f ⊣ [A::Ob, B::Ob, f::(A → B)]
  id(A) ⋅ f == f ⊣ [A::Ob, B::Ob, f::(A → B)]
end

• two type constructors, Ob (object) and Hom (morphism)
  • type Hom is a dependent type
    • depending on two objects, named dom (domain) and codom (codomain)
• two term constructors, id (identity) and compose (composition).
  • return types depend on the argument values, eg id(A) has type Hom(A,A)
  • compose also uses context variables, listed to the right of the ⊣ symbol
• @op call allows us to create method aliases that can then be used throughout the rest of the theory and outside of definition
• result of the @theory macro: a module with the following members
  • 1. for each declaration in the theory, a function named with the name of the declaration
    • declaration: includes term constructors, type constructors, arguments to type constructors (i.e. accessors like dom and codom), and aliases of the above)
    • in the above example, module ThCategory has functions Ob, Hom, dom, codom, compose, id, ⋅, →
  • 2. a submodule called Meta with members
    • T: a zero-field struct that serves as a type-level signifier for the theory.
    • theory: a constant of type GAT which stores the data of the theory.
    • @theory: a macro which expands directly to theory, which is used to pass around the data of the theory at macro-expand time.

@present (Gatlab.models.Presentations.jl)

• two methods for defining models of a GAT
  • 1. as julia objects using @instance macro
    • useful for casting generic data structures, such as matrices, abstract tensor systems, and wiring diagrams, in categorical language
  • 2. as syntactic objects using @present macro
    • define small categories by generators and relations
    • useful in applications like knowledge representation